A:Type, none:A, comb:(AAA), base:({R:Realizer| ((Rnone?(R))) & ((Rplus?(R)))} A),
R:Realizer.
case(R)Rnone: noneleft  right: comb(left,right)base(b). base(b)  A 

latex

Definitions	x,y,z,w,v. t(x;y;z;w;v), x. t(x), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z. t(x;y;z), P  Q, if b then t else f fi , ff, x,y,z,w. t(x;y;z;w), x(s), x(s1,s2), case(R)Rnone: noneleft  right: comb(left;right)base(b). base(b), t  T, Rplus?(x1), Rnone?(x1), b, A, P & Q, x:A. B(x), , False, x(s1,s2,s3,s4,s5), x(a,b,c,d,e,f), x(s1,s2,s3), x(s1,s2,s3,s4)
Lemmas	es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, finite-prob-space wf, bool wf, Rpre wf, Rsends wf, fpf wf, decl-type wf, decl-state wf, Reffect wf, IdLnk wf, Rsframe wf, Knd wf, Rframe wf, Id wf, rationals wf, Rplus? wf, Rnone? wf, assert wf, not wf, false wf, Rinit wf, es realizer ind wf